$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), $a$:$T$, $L$:$T$ List. no\_repeats($T$;$L$) $\Rightarrow$ no\_repeats($T$;insert($a$;$L$))